STM: possible-world wf

STM: feasible-frame-lemma

STM: feasible-aframe-lemma

STM: d-feasible-fair-fifo

STM: d-feasible-world

STM: ma-ds-sub

STM: ma-da-sub

STM: ma-init-sub

STM: ma-pre-sub

STM: ma-decla-sub

STM: ma-npre-sub

STM: ma-ef-sub

STM: ma-send-sub

STM: ma-frame-sub

STM: ma-aframe-sub

STM: ma-bframe-sub

STM: ma-rframe-sub

STM: ma-sframe-sub

STM: possible-world-monotonic

ABS: es is an event system of D

STM: d-es wf

ABS: D realizes es. P(es)

STM: d-realizes wf

ABS: D realizes2 es.P(es)

STM: d-realizes2 wf

STM: d-realizes2-implies-realizes

STM: init-rule

STM: frame-rule

STM: aframe-rule

STM: bframe-rule

STM: rframe-rule

STM: sframe-rule

STM: sframe-rule2

STM: effect-rule

STM: effect-rule2

STM: sends-rule

STM: better-sends-rule

STM: sends-rule2

STM: pre-rule